import static org.junit.Assert.assertEquals;
import static org.junit.Assert.assertFalse;
import static org.junit.Assert.assertSame;

import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
import java.io.File;
import java.io.IOException;

import javax.swing.Timer;

import model.BasicParameter;
import model.ParameterValue;
import model.cnf.CNF;
import model.cnf.FileCNF;
import model.solver.IllegalSolverArgumentException;
import model.solver.MiniSatParameter;
import model.solver.SolverParameter;
import model.solver.SolverResult;
import model.solver.SolverResultStatus;

import org.junit.Before;
import org.junit.Test;

import controller.solver.MiniSat;

public class TestMiniSat {

	private File	solverDirectory;
	private MiniSat	sat;

	@Before
	public void setUp() {
		try
		{
			solverDirectory = new File("solveur");

			sat = new MiniSat(solverDirectory);
		} catch (IOException e)
		{
			e.printStackTrace();
			return;
		}
	}

	@Test
	public void testMiniSat() {
		assertFalse("minisat don't use timeout", sat.hasTimeout());
	}

	@Test
	public void testGetCommandLine() {
		String cnfFile = "./tstcnf/unsat.cnf";
		MiniSatParameter param = sat.getMiniSatParameter();

		// basic parameter
		String[] tab = sat.getCommandLine(cnfFile);
		assertEquals("wrong parameter : wrong path", tab[0], sat.getPath());
		assertEquals("wrong parameter : wrong pre", tab[1], "-pre=none");
		assertEquals("wrong parameter : wrong source", tab[2], cnfFile);

		// timeout doesn't appear
		param.setTimeOut(4000);
		tab = sat.getCommandLine(cnfFile);
		assertEquals("wrong parameter : wrong path", tab[0], sat.getPath());
		assertEquals("wrong parameter : wrong pre", tab[1], "-pre=none");
		assertEquals("wrong parameter : wrong source", tab[2], cnfFile);

		// turn everything on
		// param.setAsymm(ParameterValue.TRUE); //NOT YET ;)
		param.setDecay(0.5);
		param.setGrow(1);
		param.setPolarityMode(ParameterValue.TRUE);
		param.setPre(true);
		param.setRcheck(ParameterValue.TRUE);
		param.setRndfreq(0.5);
		param.setVerbosity(2);

		tab = sat.getCommandLine(cnfFile);
		int i = 1;
		assertEquals("wrong parameter : wrong path", tab[0], sat.getPath());
		assertEquals("wrong parameter : wrong pre", tab[i++], "-pre=once");
		assertEquals("wrong parameter : wrong rcheck", tab[i++], "-rcheck=true");
		assertEquals("wrong parameter : wrong grow", tab[i++], "-grow=1");
		assertEquals("wrong parameter : wrong polarity", tab[i++], "-polarity-mode=true");
		assertEquals("wrong parameter : wrong decay", tab[i++], "-decay=0.5");
		assertEquals("wrong parameter : wrong rnd freq", tab[i++], "-rnd-freq=0.5");
		assertEquals("wrong parameter : wrong verbosity", tab[i++], "-verbosity=2");
		assertEquals("wrong parameter : wrong source", tab[i++], cnfFile);

		// change value
		// param.setAsymm(ParameterValue.TRUE); //NOT YET ;)
		param.setDecay(1);
		param.setGrow(2);
		param.setPolarityMode(ParameterValue.FALSE);
		param.setPre(false);
		param.setRcheck(ParameterValue.FALSE);
		param.setRndfreq(0);
		param.setVerbosity(0);

		tab = sat.getCommandLine(cnfFile);
		i = 1;
		assertEquals("wrong parameter : wrong path", tab[0], sat.getPath());
		assertEquals("wrong parameter : wrong pre", tab[i++], "-pre=none");
		assertEquals("wrong parameter : wrong rcheck", tab[i++], "-rcheck=false");
		assertEquals("wrong parameter : wrong grow", tab[i++], "-grow=2");
		assertEquals("wrong parameter : wrong polarity", tab[i++], "-polarity-mode=false");
		assertEquals("wrong parameter : wrong decay", tab[i++], "-decay=1.0");
		assertEquals("wrong parameter : wrong rnd freq", tab[i++], "-rnd-freq=0.0");
		assertEquals("wrong parameter : wrong verbosity", tab[i++], "-verbosity=0");
		assertEquals("wrong parameter : wrong source", tab[i++], cnfFile);

		// desactivate some of them
		// param.setAsymm(ParameterValue.TRUE); //NOT YET ;)
		param.setDecay(1);
		param.setGrow(2);
		param.setPolarityMode(ParameterValue.NOT_USED);
		param.setPre(false);
		param.setRcheck(ParameterValue.FALSE);
		param.setRndfreq(MiniSatParameter.NOT_USED);
		param.setVerbosity(0);

		tab = sat.getCommandLine(cnfFile);
		i = 1;
		assertEquals("wrong parameter : wrong path", tab[0], sat.getPath());
		assertEquals("wrong parameter : wrong pre", tab[i++], "-pre=none");
		assertEquals("wrong parameter : wrong rcheck", tab[i++], "-rcheck=false");
		assertEquals("wrong parameter : wrong grow", tab[i++], "-grow=2");
		assertEquals("wrong parameter : wrong decay", tab[i++], "-decay=1.0");
		assertEquals("wrong parameter : wrong verbosity", tab[i++], "-verbosity=0");
		assertEquals("wrong parameter : wrong source", tab[i++], cnfFile);

	}

	@Test
	public void testDetectUnsat() {
		String cnfFile = "./tstcnf/unsat.cnf";
		CNF cnf;
		try
		{
			cnf = new FileCNF(cnfFile);
		} catch (Exception e)
		{
			e.printStackTrace();
			return;
		}

		SolverResult res;
		try
		{
			res = sat.evaluate(cnf, null);
		} catch (IllegalSolverArgumentException e)
		{
			e.printStackTrace();
			return;
		}
		assertSame("doesn't detect cnf is unsat", SolverResultStatus.UNSATISFIABLE, res.getStatus());
	}

	@Test
	public void testSatInstance() {
		String cnfFile = "./tstcnf/sat.cnf";
		CNF cnf;
		try
		{
			cnf = new FileCNF(cnfFile);
		} catch (Exception e)
		{
			e.printStackTrace();
			return;
		}

		SolverResult res;
		try
		{
			res = sat.evaluate(cnf, null);
		} catch (IllegalSolverArgumentException e)
		{
			e.printStackTrace();
			return;
		}
		assertSame("doesn't detect cnf is sat", SolverResultStatus.SATISFIABLE, res.getStatus());
	}

	@Test
	public void testTimeOut() {
		String cnfFile = "./tstcnf/longue.cnf";
		SolverParameter param = sat.getMiniSatParameter();
		param.setTimeOut(BasicParameter.MIN_DELAY);
		CNF cnf;
		try
		{
			cnf = new FileCNF(cnfFile);
		} catch (Exception e)
		{
			e.printStackTrace();
			return;
		}

		SolverResult res;
		try
		{
			res = sat.evaluate(cnf, null);
		} catch (Exception e)
		{
			// e.printStackTrace();
			return;
		}
		assertSame("doesn't detect timeout", SolverResultStatus.TIMEOUT_REACHED, res.getStatus());
	}

	@Test
	public void testCNFDoesntExist() {
		String cnfFile = "./tstcnf/.cnf";
		CNF cnf;
		try
		{
			cnf = new FileCNF(cnfFile);
		} catch (Exception e)
		{
			// e.printStackTrace();
			return;
		}

		SolverResult res;
		try
		{
			res = sat.evaluate(cnf, null);
		} catch (IllegalSolverArgumentException e)
		{
			// e.printStackTrace();
			return;
		}
		assertSame("doesn't detect cnf doesn't exist", SolverResultStatus.PROBLEM, res.getStatus());
	}

	@Test
	public void testStop() {
		String cnfFile = "./tstcnf/longue.cnf";
		// String out = "./cnf/newcnf.cnf";
		// param.setTimeOut(BasicParameter.MIN_DELAY);

		CNF cnf;
		try
		{
			cnf = new FileCNF(cnfFile);
		} catch (Exception e)
		{
			e.printStackTrace();
			return;
		}

		final Timer t = new Timer(500, null);
		t.addActionListener(new ActionListener() {
			@Override
			public void actionPerformed(ActionEvent e) {
				t.stop();
				sat.stop();
			}
		});

		SolverResult res;
		try
		{
			t.start();

			res = sat.evaluate(cnf, null);
		} catch (Exception e)
		{
			e.printStackTrace();
			return;
		}
		assertSame("problem with the use of stop function", SolverResultStatus.STOP, res.getStatus());
	}

}
